B:Type, P:(B). finite-type(B)  finite-type({b:B| P(b) }) 

latex

Definitions	l[i], , AB, A, False, ||as||, A & B, SqStable(P), T, True, filter(P;l), , P  Q, P & Q, {T}, P  Q, finite-type(T), x(s), Prop, t  T, P  Q, x:A. B(x), (x  l), b, x:A. B(x)
Lemmas	l member wf, assert wf, finite-type wf, finite-type-iff-list, implies functionality wrt iff, bool wf, filter type, decidable assert, sq stable from decidable, member filter, select wf, length wf1